(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_AUFBV)
(declare-fun v0 () (_ BitVec 4))
(declare-fun a1 () (Array  (_ BitVec 9)  (_ BitVec 4)))
(assert (let ((e2(_ bv3788 13)))
(let ((e3(_ bv17564 15)))
(let ((e4 (bvshl v0 v0)))
(let ((e5 (ite (bvslt e2 e2) (_ bv1 1) (_ bv0 1))))
(let ((e6 (ite (bvsgt e3 ((_ sign_extend 11) v0)) (_ bv1 1) (_ bv0 1))))
(let ((e7 (store a1 ((_ extract 12 4) e2) ((_ sign_extend 3) e6))))
(let ((e8 (select e7 ((_ sign_extend 8) e6))))
(let ((e9 (select e7 ((_ sign_extend 5) e8))))
(let ((e10 (store e7 ((_ sign_extend 5) e8) ((_ extract 10 7) e3))))
(let ((e11 (select e7 ((_ extract 10 2) e3))))
(let ((e12 (select e10 ((_ sign_extend 5) e4))))
(let ((e13 (ite (bvsgt ((_ sign_extend 3) e5) e12) (_ bv1 1) (_ bv0 1))))
(let ((e14 (bvadd v0 ((_ zero_extend 3) e6))))
(let ((e15 (bvor e11 e11)))
(let ((e16 (ite (bvule e8 e14) (_ bv1 1) (_ bv0 1))))
(let ((e17 (ite (bvugt e5 e6) (_ bv1 1) (_ bv0 1))))
(let ((e18 (bvnot e9)))
(let ((e19 (bvlshr e18 e14)))
(let ((e20 ((_ rotate_left 2) e11)))
(let ((e21 (ite (bvslt e4 e12) (_ bv1 1) (_ bv0 1))))
(let ((e22 (bvsub e3 ((_ zero_extend 11) e8))))
(let ((e23 (bvxnor e4 ((_ sign_extend 3) e16))))
(let ((e24 (bvcomp e2 ((_ sign_extend 9) e18))))
(let ((e25 (= e23 ((_ sign_extend 3) e17))))
(let ((e26 (bvuge e3 ((_ sign_extend 11) e9))))
(let ((e27 (bvuge e23 e19)))
(let ((e28 (bvsgt e23 e18)))
(let ((e29 (bvsgt ((_ sign_extend 3) e21) e8)))
(let ((e30 (bvult ((_ sign_extend 11) e11) e3)))
(let ((e31 (= e19 ((_ sign_extend 3) e5))))
(let ((e32 (bvuge e11 ((_ sign_extend 3) e24))))
(let ((e33 (bvsle ((_ sign_extend 11) e20) e3)))
(let ((e34 (bvsge e12 e15)))
(let ((e35 (bvule ((_ sign_extend 3) e13) e9)))
(let ((e36 (= e12 e19)))
(let ((e37 (bvsge e2 ((_ zero_extend 9) e9))))
(let ((e38 (bvsle e22 ((_ zero_extend 11) e19))))
(let ((e39 (= v0 e11)))
(let ((e40 (bvslt e23 ((_ sign_extend 3) e17))))
(let ((e41 (bvsge e12 ((_ zero_extend 3) e16))))
(let ((e42 (bvugt e4 ((_ zero_extend 3) e13))))
(let ((e43 (bvsge e15 ((_ zero_extend 3) e24))))
(let ((e44 (distinct v0 v0)))
(let ((e45 (bvuge e24 e24)))
(let ((e46 (= e23 ((_ sign_extend 3) e21))))
(let ((e47 (distinct e15 v0)))
(let ((e48 (bvult e11 e14)))
(let ((e49 (bvult e4 e11)))
(let ((e50 (= e4 e14)))
(let ((e51 (bvsgt ((_ sign_extend 3) e24) e9)))
(let ((e52 (bvslt ((_ zero_extend 3) e16) e9)))
(let ((e53 (= e19 ((_ sign_extend 3) e5))))
(let ((e54 (bvsge e16 e5)))
(let ((e55 (bvuge ((_ sign_extend 3) e21) e9)))
(let ((e56 (bvslt e23 e15)))
(let ((e57 (distinct e14 e20)))
(let ((e58 (bvsge e3 ((_ zero_extend 14) e13))))
(let ((e59 (bvsle e22 e3)))
(let ((e60 (bvule ((_ sign_extend 3) e16) e14)))
(let ((e61 (= e4 ((_ sign_extend 3) e5))))
(let ((e62 (bvsle ((_ zero_extend 14) e17) e22)))
(let ((e63 (bvuge ((_ sign_extend 3) e24) e15)))
(let ((e64 (bvsle e17 e6)))
(let ((e65 (or e38 e29)))
(let ((e66 (not e54)))
(let ((e67 (and e66 e59)))
(let ((e68 (or e60 e46)))
(let ((e69 (and e55 e39)))
(let ((e70 (not e27)))
(let ((e71 (not e43)))
(let ((e72 (ite e42 e70 e40)))
(let ((e73 (and e61 e49)))
(let ((e74 (not e69)))
(let ((e75 (or e68 e32)))
(let ((e76 (and e62 e50)))
(let ((e77 (=> e75 e34)))
(let ((e78 (and e58 e73)))
(let ((e79 (= e53 e57)))
(let ((e80 (=> e52 e36)))
(let ((e81 (not e33)))
(let ((e82 (or e74 e31)))
(let ((e83 (not e80)))
(let ((e84 (or e72 e28)))
(let ((e85 (or e84 e51)))
(let ((e86 (=> e78 e67)))
(let ((e87 (xor e76 e56)))
(let ((e88 (ite e48 e37 e47)))
(let ((e89 (ite e77 e83 e41)))
(let ((e90 (= e87 e82)))
(let ((e91 (= e63 e81)))
(let ((e92 (and e88 e26)))
(let ((e93 (not e45)))
(let ((e94 (and e92 e93)))
(let ((e95 (not e64)))
(let ((e96 (or e65 e89)))
(let ((e97 (=> e90 e96)))
(let ((e98 (= e86 e30)))
(let ((e99 (ite e44 e35 e95)))
(let ((e100 (=> e85 e99)))
(let ((e101 (ite e97 e97 e25)))
(let ((e102 (xor e94 e101)))
(let ((e103 (xor e100 e79)))
(let ((e104 (= e71 e91)))
(let ((e105 (or e104 e98)))
(let ((e106 (= e105 e103)))
(let ((e107 (xor e106 e106)))
(let ((e108 (= e107 e102)))
e108
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
